H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 2.73 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ CR

mainModule List

((sort :: [Char] -> [Char]) :: [Char] -> [Char])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge

cmp xs []

merge

cmp [] ys

merge

cmp (x : xs) (y : ys)

case	x `cmp` y of
	GT	->	y : merge cmp (x : xs) ys
	_	->	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Case Reductions:
The following Case expression

case cmp x y of
GT → y : merge cmp (x : xs) ys

_ → x : merge cmp xs (y : ys)

is transformed to

merge0 y cmp x xs ys GT = y : merge cmp (x : xs) ys

merge0 y cmp x xs ys _ = x : merge cmp xs (y : ys)

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

mainModule List

((sort :: [Char] -> [Char]) :: [Char] -> [Char])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((sort :: [Char] -> [Char]) :: [Char] -> [Char])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule List

(sort :: [Char] -> [Char])

module List where

import qualified Maybe
import qualified Prelude

merge :: (a -> a -> Ordering) -> [a] -> [a] -> [a]

merge	cmp xs []	=	xs
merge	cmp [] ys	=	ys
merge	cmp (x : xs) (y : ys)	=	merge0 y cmp x xs ys (x `cmp` y)

merge0	y cmp x xs ys GT	=	y : merge cmp (x : xs) ys
merge0	y cmp x xs ys vw	=	x : merge cmp xs (y : ys)

merge_pairs :: (a -> a -> Ordering) -> [[a]] -> [[a]]

merge_pairs	cmp []	=	[]
merge_pairs	cmp (xs : [])	=	xs : []
merge_pairs	cmp (xs : ys : xss)	=	merge cmp xs ys : merge_pairs cmp xss

mergesort :: (a -> a -> Ordering) -> [a] -> [a]

mergesort

cmp

mergesort' cmp . map wrap

mergesort' :: (a -> a -> Ordering) -> [[a]] -> [a]

mergesort'	cmp []	=	[]
mergesort'	cmp (xs : [])	=	xs
mergesort'	cmp xss	=	mergesort' cmp (merge_pairs cmp xss)

sort :: Ord a => [a] -> [a]

sort

mergesort compare l

wrap :: a -> [a]

wrap

x : []

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="sort",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="sort vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="mergesort compare vz3",fontsize=16,color="black",shape="box"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="(mergesort' compare) . map wrap",fontsize=16,color="black",shape="box"];5 -> 6[label="",style="solid", color="black", weight=3];
6[label="mergesort' compare (map wrap vz3)",fontsize=16,color="burlywood",shape="box"];935[label="vz3/vz30 : vz31",fontsize=10,color="white",style="solid",shape="box"];6 -> 935[label="",style="solid", color="burlywood", weight=9];
935 -> 7[label="",style="solid", color="burlywood", weight=3];
936[label="vz3/[]",fontsize=10,color="white",style="solid",shape="box"];6 -> 936[label="",style="solid", color="burlywood", weight=9];
936 -> 8[label="",style="solid", color="burlywood", weight=3];
7[label="mergesort' compare (map wrap (vz30 : vz31))",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="mergesort' compare (map wrap [])",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="mergesort' compare (wrap vz30 : map wrap vz31)",fontsize=16,color="burlywood",shape="box"];937[label="vz31/vz310 : vz311",fontsize=10,color="white",style="solid",shape="box"];9 -> 937[label="",style="solid", color="burlywood", weight=9];
937 -> 11[label="",style="solid", color="burlywood", weight=3];
938[label="vz31/[]",fontsize=10,color="white",style="solid",shape="box"];9 -> 938[label="",style="solid", color="burlywood", weight=9];
938 -> 12[label="",style="solid", color="burlywood", weight=3];
10[label="mergesort' compare []",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mergesort' compare (wrap vz30 : map wrap (vz310 : vz311))",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mergesort' compare (wrap vz30 : map wrap [])",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13[label="[]",fontsize=16,color="green",shape="box"];14[label="mergesort' compare (wrap vz30 : wrap vz310 : map wrap vz311)",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15[label="mergesort' compare (wrap vz30 : [])",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="mergesort' compare (merge_pairs compare (wrap vz30 : wrap vz310 : map wrap vz311))",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="wrap vz30",fontsize=16,color="black",shape="triangle"];17 -> 19[label="",style="solid", color="black", weight=3];
18 -> 589[label="",style="dashed", color="red", weight=0];
18[label="mergesort' compare (merge compare (wrap vz30) (wrap vz310) : merge_pairs compare (map wrap vz311))",fontsize=16,color="magenta"];18 -> 590[label="",style="dashed", color="magenta", weight=3];
18 -> 591[label="",style="dashed", color="magenta", weight=3];
19[label="vz30 : []",fontsize=16,color="green",shape="box"];590[label="map wrap vz311",fontsize=16,color="burlywood",shape="triangle"];940[label="vz311/vz3110 : vz3111",fontsize=10,color="white",style="solid",shape="box"];590 -> 940[label="",style="solid", color="burlywood", weight=9];
940 -> 744[label="",style="solid", color="burlywood", weight=3];
941[label="vz311/[]",fontsize=10,color="white",style="solid",shape="box"];590 -> 941[label="",style="solid", color="burlywood", weight=9];
941 -> 745[label="",style="solid", color="burlywood", weight=3];
591 -> 746[label="",style="dashed", color="red", weight=0];
591[label="merge compare (wrap vz30) (wrap vz310)",fontsize=16,color="magenta"];591 -> 747[label="",style="dashed", color="magenta", weight=3];
591 -> 748[label="",style="dashed", color="magenta", weight=3];
589[label="mergesort' compare (vz78 : merge_pairs compare vz79)\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];943[label="vz79/vz790 : vz791",fontsize=10,color="white",style="solid",shape="box"];589 -> 943[label="",style="solid", color="burlywood", weight=9];
943 -> 749[label="",style="solid", color="burlywood", weight=3];
944[label="vz79/[]",fontsize=10,color="white",style="solid",shape="box"];589 -> 944[label="",style="solid", color="burlywood", weight=9];
944 -> 750[label="",style="solid", color="burlywood", weight=3];
744[label="map wrap (vz3110 : vz3111)",fontsize=16,color="black",shape="box"];744 -> 751[label="",style="solid", color="black", weight=3];
745[label="map wrap []",fontsize=16,color="black",shape="box"];745 -> 752[label="",style="solid", color="black", weight=3];
747 -> 17[label="",style="dashed", color="red", weight=0];
747[label="wrap vz310",fontsize=16,color="magenta"];747 -> 753[label="",style="dashed", color="magenta", weight=3];
748 -> 17[label="",style="dashed", color="red", weight=0];
748[label="wrap vz30",fontsize=16,color="magenta"];746[label="merge compare vz81 vz80",fontsize=16,color="burlywood",shape="triangle"];947[label="vz80/vz800 : vz801",fontsize=10,color="white",style="solid",shape="box"];746 -> 947[label="",style="solid", color="burlywood", weight=9];
947 -> 754[label="",style="solid", color="burlywood", weight=3];
948[label="vz80/[]",fontsize=10,color="white",style="solid",shape="box"];746 -> 948[label="",style="solid", color="burlywood", weight=9];
948 -> 755[label="",style="solid", color="burlywood", weight=3];
749[label="mergesort' compare (vz78 : merge_pairs compare (vz790 : vz791))\n  Ord a",fontsize=16,color="burlywood",shape="box"];949[label="vz791/vz7910 : vz7911",fontsize=10,color="white",style="solid",shape="box"];749 -> 949[label="",style="solid", color="burlywood", weight=9];
949 -> 756[label="",style="solid", color="burlywood", weight=3];
950[label="vz791/[]",fontsize=10,color="white",style="solid",shape="box"];749 -> 950[label="",style="solid", color="burlywood", weight=9];
950 -> 757[label="",style="solid", color="burlywood", weight=3];
750[label="mergesort' compare (vz78 : merge_pairs compare [])\n  Ord a",fontsize=16,color="black",shape="box"];750 -> 758[label="",style="solid", color="black", weight=3];
751[label="wrap vz3110 : map wrap vz3111",fontsize=16,color="green",shape="box"];751 -> 759[label="",style="dashed", color="green", weight=3];
751 -> 760[label="",style="dashed", color="green", weight=3];
752[label="[]",fontsize=16,color="green",shape="box"];753[label="vz310",fontsize=16,color="green",shape="box"];754[label="merge compare vz81 (vz800 : vz801)",fontsize=16,color="burlywood",shape="box"];951[label="vz81/vz810 : vz811",fontsize=10,color="white",style="solid",shape="box"];754 -> 951[label="",style="solid", color="burlywood", weight=9];
951 -> 761[label="",style="solid", color="burlywood", weight=3];
952[label="vz81/[]",fontsize=10,color="white",style="solid",shape="box"];754 -> 952[label="",style="solid", color="burlywood", weight=9];
952 -> 762[label="",style="solid", color="burlywood", weight=3];
755[label="merge compare vz81 []",fontsize=16,color="black",shape="box"];755 -> 763[label="",style="solid", color="black", weight=3];
756[label="mergesort' compare (vz78 : merge_pairs compare (vz790 : vz7910 : vz7911))\n  Ord a",fontsize=16,color="black",shape="box"];756 -> 764[label="",style="solid", color="black", weight=3];
757[label="mergesort' compare (vz78 : merge_pairs compare (vz790 : []))\n  Ord a",fontsize=16,color="black",shape="box"];757 -> 765[label="",style="solid", color="black", weight=3];
758[label="mergesort' compare (vz78 : [])\n  Ord a",fontsize=16,color="black",shape="box"];758 -> 766[label="",style="solid", color="black", weight=3];
759 -> 17[label="",style="dashed", color="red", weight=0];
759[label="wrap vz3110",fontsize=16,color="magenta"];759 -> 767[label="",style="dashed", color="magenta", weight=3];
760 -> 590[label="",style="dashed", color="red", weight=0];
760[label="map wrap vz3111",fontsize=16,color="magenta"];760 -> 768[label="",style="dashed", color="magenta", weight=3];
761[label="merge compare (vz810 : vz811) (vz800 : vz801)",fontsize=16,color="black",shape="box"];761 -> 769[label="",style="solid", color="black", weight=3];
762[label="merge compare [] (vz800 : vz801)",fontsize=16,color="black",shape="box"];762 -> 770[label="",style="solid", color="black", weight=3];
763[label="vz81",fontsize=16,color="green",shape="box"];764[label="mergesort' compare (vz78 : merge compare vz790 vz7910 : merge_pairs compare vz7911)\n  Ord a",fontsize=16,color="black",shape="box"];764 -> 771[label="",style="solid", color="black", weight=3];
765[label="mergesort' compare (vz78 : vz790 : [])\n  Ord a",fontsize=16,color="black",shape="box"];765 -> 772[label="",style="solid", color="black", weight=3];
766[label="vz78\n  Ord a",fontsize=16,color="green",shape="box"];767[label="vz3110",fontsize=16,color="green",shape="box"];768[label="vz3111",fontsize=16,color="green",shape="box"];769 -> 814[label="",style="dashed", color="red", weight=0];
769[label="merge0 vz800 compare vz810 vz811 vz801 (compare vz810 vz800)",fontsize=16,color="magenta"];769 -> 815[label="",style="dashed", color="magenta", weight=3];
769 -> 816[label="",style="dashed", color="magenta", weight=3];
769 -> 817[label="",style="dashed", color="magenta", weight=3];
769 -> 818[label="",style="dashed", color="magenta", weight=3];
769 -> 819[label="",style="dashed", color="magenta", weight=3];
770[label="vz800 : vz801",fontsize=16,color="green",shape="box"];771[label="mergesort' compare (merge_pairs compare (vz78 : merge compare vz790 vz7910 : merge_pairs compare vz7911))\n  Ord a",fontsize=16,color="black",shape="box"];771 -> 774[label="",style="solid", color="black", weight=3];
772[label="mergesort' compare (merge_pairs compare (vz78 : vz790 : []))\n  Ord a",fontsize=16,color="black",shape="box"];772 -> 775[label="",style="solid", color="black", weight=3];
815[label="vz801",fontsize=16,color="green",shape="box"];816[label="vz811",fontsize=16,color="green",shape="box"];817[label="vz810",fontsize=16,color="green",shape="box"];818[label="compare vz810 vz800",fontsize=16,color="black",shape="triangle"];818 -> 830[label="",style="solid", color="black", weight=3];
819[label="vz800",fontsize=16,color="green",shape="box"];814[label="merge0 vz88 compare vz89 vz90 vz91 vz92\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];956[label="vz92/LT",fontsize=10,color="white",style="solid",shape="box"];814 -> 956[label="",style="solid", color="burlywood", weight=9];
956 -> 831[label="",style="solid", color="burlywood", weight=3];
957[label="vz92/EQ",fontsize=10,color="white",style="solid",shape="box"];814 -> 957[label="",style="solid", color="burlywood", weight=9];
957 -> 832[label="",style="solid", color="burlywood", weight=3];
958[label="vz92/GT",fontsize=10,color="white",style="solid",shape="box"];814 -> 958[label="",style="solid", color="burlywood", weight=9];
958 -> 833[label="",style="solid", color="burlywood", weight=3];
774 -> 589[label="",style="dashed", color="red", weight=0];
774[label="mergesort' compare (merge compare vz78 (merge compare vz790 vz7910) : merge_pairs compare (merge_pairs compare vz7911))\n  Ord a",fontsize=16,color="magenta"];774 -> 777[label="",style="dashed", color="magenta", weight=3];
774 -> 778[label="",style="dashed", color="magenta", weight=3];
775 -> 589[label="",style="dashed", color="red", weight=0];
775[label="mergesort' compare (merge compare vz78 vz790 : merge_pairs compare [])\n  Ord a",fontsize=16,color="magenta"];775 -> 779[label="",style="dashed", color="magenta", weight=3];
775 -> 780[label="",style="dashed", color="magenta", weight=3];
830[label="primCmpChar vz810 vz800",fontsize=16,color="burlywood",shape="box"];961[label="vz810/Char vz8100",fontsize=10,color="white",style="solid",shape="box"];830 -> 961[label="",style="solid", color="burlywood", weight=9];
961 -> 865[label="",style="solid", color="burlywood", weight=3];
831[label="merge0 vz88 compare vz89 vz90 vz91 LT\n  Ord a",fontsize=16,color="black",shape="box"];831 -> 866[label="",style="solid", color="black", weight=3];
832[label="merge0 vz88 compare vz89 vz90 vz91 EQ\n  Ord a",fontsize=16,color="black",shape="box"];832 -> 867[label="",style="solid", color="black", weight=3];
833[label="merge0 vz88 compare vz89 vz90 vz91 GT\n  Ord a",fontsize=16,color="black",shape="box"];833 -> 868[label="",style="solid", color="black", weight=3];
777[label="merge_pairs compare vz7911\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];962[label="vz7911/vz79110 : vz79111",fontsize=10,color="white",style="solid",shape="box"];777 -> 962[label="",style="solid", color="burlywood", weight=9];
962 -> 782[label="",style="solid", color="burlywood", weight=3];
963[label="vz7911/[]",fontsize=10,color="white",style="solid",shape="box"];777 -> 963[label="",style="solid", color="burlywood", weight=9];
963 -> 783[label="",style="solid", color="burlywood", weight=3];
778[label="merge compare vz78 (merge compare vz790 vz7910)\n  Ord a",fontsize=16,color="burlywood",shape="box"];964[label="vz7910/vz79100 : vz79101",fontsize=10,color="white",style="solid",shape="box"];778 -> 964[label="",style="solid", color="burlywood", weight=9];
964 -> 784[label="",style="solid", color="burlywood", weight=3];
965[label="vz7910/[]",fontsize=10,color="white",style="solid",shape="box"];778 -> 965[label="",style="solid", color="burlywood", weight=9];
965 -> 785[label="",style="solid", color="burlywood", weight=3];
779[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];780[label="merge compare vz78 vz790\n  Ord a",fontsize=16,color="burlywood",shape="triangle"];966[label="vz790/vz7900 : vz7901",fontsize=10,color="white",style="solid",shape="box"];780 -> 966[label="",style="solid", color="burlywood", weight=9];
966 -> 786[label="",style="solid", color="burlywood", weight=3];
967[label="vz790/[]",fontsize=10,color="white",style="solid",shape="box"];780 -> 967[label="",style="solid", color="burlywood", weight=9];
967 -> 787[label="",style="solid", color="burlywood", weight=3];
865[label="primCmpChar (Char vz8100) vz800",fontsize=16,color="burlywood",shape="box"];968[label="vz800/Char vz8000",fontsize=10,color="white",style="solid",shape="box"];865 -> 968[label="",style="solid", color="burlywood", weight=9];
968 -> 912[label="",style="solid", color="burlywood", weight=3];
866[label="vz89 : merge compare vz90 (vz88 : vz91)\n  Ord a",fontsize=16,color="green",shape="box"];866 -> 913[label="",style="dashed", color="green", weight=3];
867[label="vz89 : merge compare vz90 (vz88 : vz91)\n  Ord a",fontsize=16,color="green",shape="box"];867 -> 914[label="",style="dashed", color="green", weight=3];
868[label="vz88 : merge compare (vz89 : vz90) vz91\n  Ord a",fontsize=16,color="green",shape="box"];868 -> 915[label="",style="dashed", color="green", weight=3];
782[label="merge_pairs compare (vz79110 : vz79111)\n  Ord a",fontsize=16,color="burlywood",shape="box"];969[label="vz79111/vz791110 : vz791111",fontsize=10,color="white",style="solid",shape="box"];782 -> 969[label="",style="solid", color="burlywood", weight=9];
969 -> 789[label="",style="solid", color="burlywood", weight=3];
970[label="vz79111/[]",fontsize=10,color="white",style="solid",shape="box"];782 -> 970[label="",style="solid", color="burlywood", weight=9];
970 -> 790[label="",style="solid", color="burlywood", weight=3];
783[label="merge_pairs compare []\n  Ord a",fontsize=16,color="black",shape="box"];783 -> 791[label="",style="solid", color="black", weight=3];
784[label="merge compare vz78 (merge compare vz790 (vz79100 : vz79101))\n  Ord a",fontsize=16,color="burlywood",shape="box"];971[label="vz790/vz7900 : vz7901",fontsize=10,color="white",style="solid",shape="box"];784 -> 971[label="",style="solid", color="burlywood", weight=9];
971 -> 792[label="",style="solid", color="burlywood", weight=3];
972[label="vz790/[]",fontsize=10,color="white",style="solid",shape="box"];784 -> 972[label="",style="solid", color="burlywood", weight=9];
972 -> 793[label="",style="solid", color="burlywood", weight=3];
785[label="merge compare vz78 (merge compare vz790 [])\n  Ord a",fontsize=16,color="black",shape="box"];785 -> 794[label="",style="solid", color="black", weight=3];
786[label="merge compare vz78 (vz7900 : vz7901)\n  Ord a",fontsize=16,color="burlywood",shape="box"];973[label="vz78/vz780 : vz781",fontsize=10,color="white",style="solid",shape="box"];786 -> 973[label="",style="solid", color="burlywood", weight=9];
973 -> 795[label="",style="solid", color="burlywood", weight=3];
974[label="vz78/[]",fontsize=10,color="white",style="solid",shape="box"];786 -> 974[label="",style="solid", color="burlywood", weight=9];
974 -> 796[label="",style="solid", color="burlywood", weight=3];
787[label="merge compare vz78 []\n  Ord a",fontsize=16,color="black",shape="box"];787 -> 797[label="",style="solid", color="black", weight=3];
912[label="primCmpChar (Char vz8100) (Char vz8000)",fontsize=16,color="black",shape="box"];912 -> 916[label="",style="solid", color="black", weight=3];
913 -> 780[label="",style="dashed", color="red", weight=0];
913[label="merge compare vz90 (vz88 : vz91)\n  Ord a",fontsize=16,color="magenta"];913 -> 917[label="",style="dashed", color="magenta", weight=3];
913 -> 918[label="",style="dashed", color="magenta", weight=3];
914 -> 780[label="",style="dashed", color="red", weight=0];
914[label="merge compare vz90 (vz88 : vz91)\n  Ord a",fontsize=16,color="magenta"];914 -> 919[label="",style="dashed", color="magenta", weight=3];
914 -> 920[label="",style="dashed", color="magenta", weight=3];
915 -> 780[label="",style="dashed", color="red", weight=0];
915[label="merge compare (vz89 : vz90) vz91\n  Ord a",fontsize=16,color="magenta"];915 -> 921[label="",style="dashed", color="magenta", weight=3];
915 -> 922[label="",style="dashed", color="magenta", weight=3];
789[label="merge_pairs compare (vz79110 : vz791110 : vz791111)\n  Ord a",fontsize=16,color="black",shape="box"];789 -> 800[label="",style="solid", color="black", weight=3];
790[label="merge_pairs compare (vz79110 : [])\n  Ord a",fontsize=16,color="black",shape="box"];790 -> 801[label="",style="solid", color="black", weight=3];
791[label="[]\n  Ord a",fontsize=16,color="green",shape="box"];792[label="merge compare vz78 (merge compare (vz7900 : vz7901) (vz79100 : vz79101))\n  Ord a",fontsize=16,color="black",shape="box"];792 -> 802[label="",style="solid", color="black", weight=3];
793[label="merge compare vz78 (merge compare [] (vz79100 : vz79101))\n  Ord a",fontsize=16,color="black",shape="box"];793 -> 803[label="",style="solid", color="black", weight=3];
794 -> 780[label="",style="dashed", color="red", weight=0];
794[label="merge compare vz78 vz790\n  Ord a",fontsize=16,color="magenta"];795[label="merge compare (vz780 : vz781) (vz7900 : vz7901)\n  Ord a",fontsize=16,color="black",shape="box"];795 -> 804[label="",style="solid", color="black", weight=3];
796[label="merge compare [] (vz7900 : vz7901)\n  Ord a",fontsize=16,color="black",shape="box"];796 -> 805[label="",style="solid", color="black", weight=3];
797[label="vz78\n  Ord a",fontsize=16,color="green",shape="box"];916[label="primCmpNat vz8100 vz8000",fontsize=16,color="burlywood",shape="triangle"];979[label="vz8100/Succ vz81000",fontsize=10,color="white",style="solid",shape="box"];916 -> 979[label="",style="solid", color="burlywood", weight=9];
979 -> 923[label="",style="solid", color="burlywood", weight=3];
980[label="vz8100/Zero",fontsize=10,color="white",style="solid",shape="box"];916 -> 980[label="",style="solid", color="burlywood", weight=9];
980 -> 924[label="",style="solid", color="burlywood", weight=3];
917[label="vz88 : vz91\n  Ord a",fontsize=16,color="green",shape="box"];918[label="vz90\n  Ord a",fontsize=16,color="green",shape="box"];919[label="vz88 : vz91\n  Ord a",fontsize=16,color="green",shape="box"];920[label="vz90\n  Ord a",fontsize=16,color="green",shape="box"];921[label="vz91\n  Ord a",fontsize=16,color="green",shape="box"];922[label="vz89 : vz90\n  Ord a",fontsize=16,color="green",shape="box"];800[label="merge compare vz79110 vz791110 : merge_pairs compare vz791111\n  Ord a",fontsize=16,color="green",shape="box"];800 -> 810[label="",style="dashed", color="green", weight=3];
800 -> 811[label="",style="dashed", color="green", weight=3];
801[label="vz79110 : []\n  Ord a",fontsize=16,color="green",shape="box"];802 -> 780[label="",style="dashed", color="red", weight=0];
802[label="merge compare vz78 (merge0 vz79100 compare vz7900 vz7901 vz79101 (compare vz7900 vz79100))\n  Ord a",fontsize=16,color="magenta"];802 -> 812[label="",style="dashed", color="magenta", weight=3];
803 -> 780[label="",style="dashed", color="red", weight=0];
803[label="merge compare vz78 (vz79100 : vz79101)\n  Ord a",fontsize=16,color="magenta"];803 -> 813[label="",style="dashed", color="magenta", weight=3];
804 -> 814[label="",style="dashed", color="red", weight=0];
804[label="merge0 vz7900 compare vz780 vz781 vz7901 (compare vz780 vz7900)\n  Ord a",fontsize=16,color="magenta"];804 -> 820[label="",style="dashed", color="magenta", weight=3];
804 -> 821[label="",style="dashed", color="magenta", weight=3];
804 -> 822[label="",style="dashed", color="magenta", weight=3];
804 -> 823[label="",style="dashed", color="magenta", weight=3];
804 -> 824[label="",style="dashed", color="magenta", weight=3];
805[label="vz7900 : vz7901\n  Ord a",fontsize=16,color="green",shape="box"];923[label="primCmpNat (Succ vz81000) vz8000",fontsize=16,color="burlywood",shape="box"];984[label="vz8000/Succ vz80000",fontsize=10,color="white",style="solid",shape="box"];923 -> 984[label="",style="solid", color="burlywood", weight=9];
984 -> 925[label="",style="solid", color="burlywood", weight=3];
985[label="vz8000/Zero",fontsize=10,color="white",style="solid",shape="box"];923 -> 985[label="",style="solid", color="burlywood", weight=9];
985 -> 926[label="",style="solid", color="burlywood", weight=3];
924[label="primCmpNat Zero vz8000",fontsize=16,color="burlywood",shape="box"];986[label="vz8000/Succ vz80000",fontsize=10,color="white",style="solid",shape="box"];924 -> 986[label="",style="solid", color="burlywood", weight=9];
986 -> 927[label="",style="solid", color="burlywood", weight=3];
987[label="vz8000/Zero",fontsize=10,color="white",style="solid",shape="box"];924 -> 987[label="",style="solid", color="burlywood", weight=9];
987 -> 928[label="",style="solid", color="burlywood", weight=3];
810 -> 780[label="",style="dashed", color="red", weight=0];
810[label="merge compare vz79110 vz791110\n  Ord a",fontsize=16,color="magenta"];810 -> 834[label="",style="dashed", color="magenta", weight=3];
810 -> 835[label="",style="dashed", color="magenta", weight=3];
811 -> 777[label="",style="dashed", color="red", weight=0];
811[label="merge_pairs compare vz791111\n  Ord a",fontsize=16,color="magenta"];811 -> 836[label="",style="dashed", color="magenta", weight=3];
812 -> 814[label="",style="dashed", color="red", weight=0];
812[label="merge0 vz79100 compare vz7900 vz7901 vz79101 (compare vz7900 vz79100)\n  Ord a",fontsize=16,color="magenta"];812 -> 825[label="",style="dashed", color="magenta", weight=3];
812 -> 826[label="",style="dashed", color="magenta", weight=3];
812 -> 827[label="",style="dashed", color="magenta", weight=3];
812 -> 828[label="",style="dashed", color="magenta", weight=3];
812 -> 829[label="",style="dashed", color="magenta", weight=3];
813[label="vz79100 : vz79101\n  Ord a",fontsize=16,color="green",shape="box"];820[label="vz7901\n  Ord a",fontsize=16,color="green",shape="box"];821[label="vz781\n  Ord a",fontsize=16,color="green",shape="box"];822[label="vz780\n  Ord a",fontsize=16,color="green",shape="box"];823[label="compare vz780 vz7900\n  Ord a",fontsize=16,color="blue",shape="box"];991[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 991[label="",style="solid", color="blue", weight=9];
991 -> 837[label="",style="solid", color="blue", weight=3];
992[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 992[label="",style="solid", color="blue", weight=9];
992 -> 838[label="",style="solid", color="blue", weight=3];
993[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 993[label="",style="solid", color="blue", weight=9];
993 -> 839[label="",style="solid", color="blue", weight=3];
994[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 994[label="",style="solid", color="blue", weight=9];
994 -> 840[label="",style="solid", color="blue", weight=3];
995[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 995[label="",style="solid", color="blue", weight=9];
995 -> 841[label="",style="solid", color="blue", weight=3];
996[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 996[label="",style="solid", color="blue", weight=9];
996 -> 842[label="",style="solid", color="blue", weight=3];
997[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 997[label="",style="solid", color="blue", weight=9];
997 -> 843[label="",style="solid", color="blue", weight=3];
998[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 998[label="",style="solid", color="blue", weight=9];
998 -> 844[label="",style="solid", color="blue", weight=3];
999[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 999[label="",style="solid", color="blue", weight=9];
999 -> 845[label="",style="solid", color="blue", weight=3];
1000[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 1000[label="",style="solid", color="blue", weight=9];
1000 -> 846[label="",style="solid", color="blue", weight=3];
1001[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 1001[label="",style="solid", color="blue", weight=9];
1001 -> 847[label="",style="solid", color="blue", weight=3];
1002[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 1002[label="",style="solid", color="blue", weight=9];
1002 -> 848[label="",style="solid", color="blue", weight=3];
1003[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 1003[label="",style="solid", color="blue", weight=9];
1003 -> 849[label="",style="solid", color="blue", weight=3];
1004[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];823 -> 1004[label="",style="solid", color="blue", weight=9];
1004 -> 850[label="",style="solid", color="blue", weight=3];
824[label="vz7900\n  Ord a",fontsize=16,color="green",shape="box"];925[label="primCmpNat (Succ vz81000) (Succ vz80000)",fontsize=16,color="black",shape="box"];925 -> 929[label="",style="solid", color="black", weight=3];
926[label="primCmpNat (Succ vz81000) Zero",fontsize=16,color="black",shape="box"];926 -> 930[label="",style="solid", color="black", weight=3];
927[label="primCmpNat Zero (Succ vz80000)",fontsize=16,color="black",shape="box"];927 -> 931[label="",style="solid", color="black", weight=3];
928[label="primCmpNat Zero Zero",fontsize=16,color="black",shape="box"];928 -> 932[label="",style="solid", color="black", weight=3];
834[label="vz791110\n  Ord a",fontsize=16,color="green",shape="box"];835[label="vz79110\n  Ord a",fontsize=16,color="green",shape="box"];836[label="vz791111\n  Ord a",fontsize=16,color="green",shape="box"];825[label="vz79101\n  Ord a",fontsize=16,color="green",shape="box"];826[label="vz7901\n  Ord a",fontsize=16,color="green",shape="box"];827[label="vz7900\n  Ord a",fontsize=16,color="green",shape="box"];828[label="compare vz7900 vz79100\n  Ord a",fontsize=16,color="blue",shape="box"];1005[label="compare :: Integer -> Integer -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1005[label="",style="solid", color="blue", weight=9];
1005 -> 851[label="",style="solid", color="blue", weight=3];
1006[label="compare :: ((@3) a b c) -> ((@3) a b c) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1006[label="",style="solid", color="blue", weight=9];
1006 -> 852[label="",style="solid", color="blue", weight=3];
1007[label="compare :: ([] a) -> ([] a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1007[label="",style="solid", color="blue", weight=9];
1007 -> 853[label="",style="solid", color="blue", weight=3];
1008[label="compare :: () -> () -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1008[label="",style="solid", color="blue", weight=9];
1008 -> 854[label="",style="solid", color="blue", weight=3];
1009[label="compare :: (Ratio a) -> (Ratio a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1009[label="",style="solid", color="blue", weight=9];
1009 -> 855[label="",style="solid", color="blue", weight=3];
1010[label="compare :: Int -> Int -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1010[label="",style="solid", color="blue", weight=9];
1010 -> 856[label="",style="solid", color="blue", weight=3];
1011[label="compare :: Bool -> Bool -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1011[label="",style="solid", color="blue", weight=9];
1011 -> 857[label="",style="solid", color="blue", weight=3];
1012[label="compare :: Ordering -> Ordering -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1012[label="",style="solid", color="blue", weight=9];
1012 -> 858[label="",style="solid", color="blue", weight=3];
1013[label="compare :: ((@2) a b) -> ((@2) a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1013[label="",style="solid", color="blue", weight=9];
1013 -> 859[label="",style="solid", color="blue", weight=3];
1014[label="compare :: (Maybe a) -> (Maybe a) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1014[label="",style="solid", color="blue", weight=9];
1014 -> 860[label="",style="solid", color="blue", weight=3];
1015[label="compare :: Float -> Float -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1015[label="",style="solid", color="blue", weight=9];
1015 -> 861[label="",style="solid", color="blue", weight=3];
1016[label="compare :: Double -> Double -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1016[label="",style="solid", color="blue", weight=9];
1016 -> 862[label="",style="solid", color="blue", weight=3];
1017[label="compare :: (Either a b) -> (Either a b) -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1017[label="",style="solid", color="blue", weight=9];
1017 -> 863[label="",style="solid", color="blue", weight=3];
1018[label="compare :: Char -> Char -> Ordering",fontsize=10,color="white",style="solid",shape="box"];828 -> 1018[label="",style="solid", color="blue", weight=9];
1018 -> 864[label="",style="solid", color="blue", weight=3];
829[label="vz79100\n  Ord a",fontsize=16,color="green",shape="box"];837[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];837 -> 869[label="",style="solid", color="black", weight=3];
838[label="compare vz780 vz7900\n  Ord a  Ord b  Ord c",fontsize=16,color="black",shape="triangle"];838 -> 870[label="",style="solid", color="black", weight=3];
839[label="compare vz780 vz7900\n  Ord a",fontsize=16,color="black",shape="triangle"];839 -> 871[label="",style="solid", color="black", weight=3];
840[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];840 -> 872[label="",style="solid", color="black", weight=3];
841[label="compare vz780 vz7900\n  Integral a",fontsize=16,color="black",shape="triangle"];841 -> 873[label="",style="solid", color="black", weight=3];
842[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];842 -> 874[label="",style="solid", color="black", weight=3];
843[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];843 -> 875[label="",style="solid", color="black", weight=3];
844[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];844 -> 876[label="",style="solid", color="black", weight=3];
845[label="compare vz780 vz7900\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];845 -> 877[label="",style="solid", color="black", weight=3];
846[label="compare vz780 vz7900\n  Ord a",fontsize=16,color="black",shape="triangle"];846 -> 878[label="",style="solid", color="black", weight=3];
847[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];847 -> 879[label="",style="solid", color="black", weight=3];
848[label="compare vz780 vz7900",fontsize=16,color="black",shape="triangle"];848 -> 880[label="",style="solid", color="black", weight=3];
849[label="compare vz780 vz7900\n  Ord a  Ord b",fontsize=16,color="black",shape="triangle"];849 -> 881[label="",style="solid", color="black", weight=3];
850 -> 818[label="",style="dashed", color="red", weight=0];
850[label="compare vz780 vz7900",fontsize=16,color="magenta"];850 -> 882[label="",style="dashed", color="magenta", weight=3];
850 -> 883[label="",style="dashed", color="magenta", weight=3];
929 -> 916[label="",style="dashed", color="red", weight=0];
929[label="primCmpNat vz81000 vz80000",fontsize=16,color="magenta"];929 -> 933[label="",style="dashed", color="magenta", weight=3];
929 -> 934[label="",style="dashed", color="magenta", weight=3];
930[label="GT",fontsize=16,color="green",shape="box"];931[label="LT",fontsize=16,color="green",shape="box"];932[label="EQ",fontsize=16,color="green",shape="box"];851 -> 837[label="",style="dashed", color="red", weight=0];
851[label="compare vz7900 vz79100",fontsize=16,color="magenta"];851 -> 884[label="",style="dashed", color="magenta", weight=3];
851 -> 885[label="",style="dashed", color="magenta", weight=3];
852 -> 838[label="",style="dashed", color="red", weight=0];
852[label="compare vz7900 vz79100\n  Ord a  Ord b  Ord c",fontsize=16,color="magenta"];852 -> 886[label="",style="dashed", color="magenta", weight=3];
852 -> 887[label="",style="dashed", color="magenta", weight=3];
853 -> 839[label="",style="dashed", color="red", weight=0];
853[label="compare vz7900 vz79100\n  Ord a",fontsize=16,color="magenta"];853 -> 888[label="",style="dashed", color="magenta", weight=3];
853 -> 889[label="",style="dashed", color="magenta", weight=3];
854 -> 840[label="",style="dashed", color="red", weight=0];
854[label="compare vz7900 vz79100",fontsize=16,color="magenta"];854 -> 890[label="",style="dashed", color="magenta", weight=3];
854 -> 891[label="",style="dashed", color="magenta", weight=3];
855 -> 841[label="",style="dashed", color="red", weight=0];
855[label="compare vz7900 vz79100\n  Integral a",fontsize=16,color="magenta"];855 -> 892[label="",style="dashed", color="magenta", weight=3];
855 -> 893[label="",style="dashed", color="magenta", weight=3];
856 -> 842[label="",style="dashed", color="red", weight=0];
856[label="compare vz7900 vz79100",fontsize=16,color="magenta"];856 -> 894[label="",style="dashed", color="magenta", weight=3];
856 -> 895[label="",style="dashed", color="magenta", weight=3];
857 -> 843[label="",style="dashed", color="red", weight=0];
857[label="compare vz7900 vz79100",fontsize=16,color="magenta"];857 -> 896[label="",style="dashed", color="magenta", weight=3];
857 -> 897[label="",style="dashed", color="magenta", weight=3];
858 -> 844[label="",style="dashed", color="red", weight=0];
858[label="compare vz7900 vz79100",fontsize=16,color="magenta"];858 -> 898[label="",style="dashed", color="magenta", weight=3];
858 -> 899[label="",style="dashed", color="magenta", weight=3];
859 -> 845[label="",style="dashed", color="red", weight=0];
859[label="compare vz7900 vz79100\n  Ord a  Ord b",fontsize=16,color="magenta"];859 -> 900[label="",style="dashed", color="magenta", weight=3];
859 -> 901[label="",style="dashed", color="magenta", weight=3];
860 -> 846[label="",style="dashed", color="red", weight=0];
860[label="compare vz7900 vz79100\n  Ord a",fontsize=16,color="magenta"];860 -> 902[label="",style="dashed", color="magenta", weight=3];
860 -> 903[label="",style="dashed", color="magenta", weight=3];
861 -> 847[label="",style="dashed", color="red", weight=0];
861[label="compare vz7900 vz79100",fontsize=16,color="magenta"];861 -> 904[label="",style="dashed", color="magenta", weight=3];
861 -> 905[label="",style="dashed", color="magenta", weight=3];
862 -> 848[label="",style="dashed", color="red", weight=0];
862[label="compare vz7900 vz79100",fontsize=16,color="magenta"];862 -> 906[label="",style="dashed", color="magenta", weight=3];
862 -> 907[label="",style="dashed", color="magenta", weight=3];
863 -> 849[label="",style="dashed", color="red", weight=0];
863[label="compare vz7900 vz79100\n  Ord a  Ord b",fontsize=16,color="magenta"];863 -> 908[label="",style="dashed", color="magenta", weight=3];
863 -> 909[label="",style="dashed", color="magenta", weight=3];
864 -> 818[label="",style="dashed", color="red", weight=0];
864[label="compare vz7900 vz79100",fontsize=16,color="magenta"];864 -> 910[label="",style="dashed", color="magenta", weight=3];
864 -> 911[label="",style="dashed", color="magenta", weight=3];
869[label="error []",fontsize=16,color="red",shape="box"];870[label="error []",fontsize=16,color="red",shape="box"];871[label="error []",fontsize=16,color="red",shape="box"];872[label="error []",fontsize=16,color="red",shape="box"];873[label="error []",fontsize=16,color="red",shape="box"];874[label="error []",fontsize=16,color="red",shape="box"];875[label="error []",fontsize=16,color="red",shape="box"];876[label="error []",fontsize=16,color="red",shape="box"];877[label="error []",fontsize=16,color="red",shape="box"];878[label="error []",fontsize=16,color="red",shape="box"];879[label="error []",fontsize=16,color="red",shape="box"];880[label="error []",fontsize=16,color="red",shape="box"];881[label="error []",fontsize=16,color="red",shape="box"];882[label="vz780",fontsize=16,color="green",shape="box"];883[label="vz7900",fontsize=16,color="green",shape="box"];933[label="vz81000",fontsize=16,color="green",shape="box"];934[label="vz80000",fontsize=16,color="green",shape="box"];884[label="vz79100",fontsize=16,color="green",shape="box"];885[label="vz7900",fontsize=16,color="green",shape="box"];886[label="vz79100\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];887[label="vz7900\n  Ord a  Ord b  Ord c",fontsize=16,color="green",shape="box"];888[label="vz79100\n  Ord a",fontsize=16,color="green",shape="box"];889[label="vz7900\n  Ord a",fontsize=16,color="green",shape="box"];890[label="vz79100",fontsize=16,color="green",shape="box"];891[label="vz7900",fontsize=16,color="green",shape="box"];892[label="vz79100\n  Integral a",fontsize=16,color="green",shape="box"];893[label="vz7900\n  Integral a",fontsize=16,color="green",shape="box"];894[label="vz79100",fontsize=16,color="green",shape="box"];895[label="vz7900",fontsize=16,color="green",shape="box"];896[label="vz79100",fontsize=16,color="green",shape="box"];897[label="vz7900",fontsize=16,color="green",shape="box"];898[label="vz79100",fontsize=16,color="green",shape="box"];899[label="vz7900",fontsize=16,color="green",shape="box"];900[label="vz79100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];901[label="vz7900\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];902[label="vz79100\n  Ord a",fontsize=16,color="green",shape="box"];903[label="vz7900\n  Ord a",fontsize=16,color="green",shape="box"];904[label="vz79100",fontsize=16,color="green",shape="box"];905[label="vz7900",fontsize=16,color="green",shape="box"];906[label="vz79100",fontsize=16,color="green",shape="box"];907[label="vz7900",fontsize=16,color="green",shape="box"];908[label="vz79100\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];909[label="vz7900\n  Ord a  Ord b",fontsize=16,color="green",shape="box"];910[label="vz7900",fontsize=16,color="green",shape="box"];911[label="vz79100",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_map(:(vz3110, vz3111)) → new_map(vz3111)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_map(:(vz3110, vz3111)) → new_map(vz3111)
The graph contains the following edges 1 > 1

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primCmpNat(Succ(vz81000), Succ(vz80000)) → new_primCmpNat(vz81000, vz80000)

From the DPs we obtained the following set of size-change graphs:

new_primCmpNat(Succ(vz81000), Succ(vz80000)) → new_primCmpNat(vz81000, vz80000)
The graph contains the following edges 1 > 1, 2 > 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz88, vz89, vz90, vz91, GT, ba) → new_merge(:(vz89, vz90), vz91, ba)
new_merge0(vz88, vz89, vz90, vz91, EQ, ba) → new_merge(vz90, :(vz88, vz91), ba)
new_merge(:(vz780, vz781), :(vz7900, vz7901), bb) → new_merge0(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, bb), bb)
new_merge0(vz88, vz89, vz90, vz91, LT, ba) → new_merge(vz90, :(vz88, vz91), ba)

The TRS R consists of the following rules:

new_compare2(vz780, vz7900, bc) → error([])
new_compare(vz780, vz7900, app(ty_[], bd)) → new_compare3(vz780, vz7900, bd)
new_compare(vz780, vz7900, app(ty_Ratio, bc)) → new_compare2(vz780, vz7900, bc)
new_compare7(vz780, vz7900, bh, ca) → error([])
new_compare0(vz780, vz7900) → error([])
new_compare4(vz780, vz7900, be, bf, bg) → error([])
new_compare10(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Integer) → new_compare0(vz780, vz7900)
new_compare3(vz780, vz7900, bd) → error([])
new_compare(vz780, vz7900, ty_Float) → new_compare5(vz780, vz7900)
new_compare(vz780, vz7900, ty_Char) → new_compare13(vz780, vz7900)
new_compare13(Char(vz8100), Char(vz8000)) → new_primCmpNat0(vz8100, vz8000)
new_compare(vz780, vz7900, app(app(ty_Either, bh), ca)) → new_compare7(vz780, vz7900, bh, ca)
new_compare1(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Bool) → new_compare10(vz780, vz7900)
new_compare6(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_@0) → new_compare1(vz780, vz7900)
new_compare(vz780, vz7900, app(ty_Maybe, cb)) → new_compare8(vz780, vz7900, cb)
new_compare8(vz780, vz7900, cb) → error([])
new_compare5(vz780, vz7900) → error([])
new_primCmpNat0(Zero, Succ(vz80000)) → LT
new_compare12(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Double) → new_compare12(vz780, vz7900)
new_compare(vz780, vz7900, app(app(app(ty_@3, be), bf), bg)) → new_compare4(vz780, vz7900, be, bf, bg)
new_compare9(vz780, vz7900) → error([])
new_primCmpNat0(Succ(vz81000), Succ(vz80000)) → new_primCmpNat0(vz81000, vz80000)
new_compare(vz780, vz7900, app(app(ty_@2, cc), cd)) → new_compare11(vz780, vz7900, cc, cd)
new_compare11(vz780, vz7900, cc, cd) → error([])
new_primCmpNat0(Zero, Zero) → EQ
new_compare(vz780, vz7900, ty_Ordering) → new_compare6(vz780, vz7900)
new_compare(vz780, vz7900, ty_Int) → new_compare9(vz780, vz7900)
new_primCmpNat0(Succ(vz81000), Zero) → GT

The set Q consists of the following terms:

new_primCmpNat0(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare3(x0, x1, x2)
new_compare5(x0, x1)
new_compare1(x0, x1)
new_primCmpNat0(Zero, Zero)
new_compare(x0, x1, ty_Bool)
new_compare(x0, x1, ty_Float)
new_primCmpNat0(Succ(x0), Succ(x1))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, ty_Ordering)
new_compare12(x0, x1)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, app(ty_[], x2))
new_compare10(x0, x1)
new_compare(x0, x1, ty_@0)
new_compare2(x0, x1, x2)
new_compare4(x0, x1, x2, x3, x4)
new_compare0(x0, x1)
new_compare11(x0, x1, x2, x3)
new_compare(x0, x1, ty_Int)
new_compare(x0, x1, ty_Char)
new_compare9(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare8(x0, x1, x2)
new_compare7(x0, x1, x2, x3)
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(Char(x0), Char(x1))
new_primCmpNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_merge0(vz88, vz89, vz90, vz91, EQ, ba) → new_merge(vz90, :(vz88, vz91), ba)
new_merge0(vz88, vz89, vz90, vz91, LT, ba) → new_merge(vz90, :(vz88, vz91), ba)

The remaining pairs can at least be oriented weakly.

new_merge0(vz88, vz89, vz90, vz91, GT, ba) → new_merge(:(vz89, vz90), vz91, ba)
new_merge(:(vz780, vz781), :(vz7900, vz7901), bb) → new_merge0(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, bb), bb)

Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(Char(x₁)) = 0
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL(Succ(x₁)) = 0
POL(Zero) = 0
POL([]) = 0
POL(app(x₁, x₂)) = 0
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 0
POL(new_compare0(x₁, x₂)) = 0
POL(new_compare1(x₁, x₂)) = 0
POL(new_compare10(x₁, x₂)) = 0
POL(new_compare11(x₁, x₂, x₃, x₄)) = 0
POL(new_compare12(x₁, x₂)) = 0
POL(new_compare13(x₁, x₂)) = 0
POL(new_compare2(x₁, x₂, x₃)) = 0
POL(new_compare3(x₁, x₂, x₃)) = 0
POL(new_compare4(x₁, x₂, x₃, x₄, x₅)) = 0
POL(new_compare5(x₁, x₂)) = 0
POL(new_compare6(x₁, x₂)) = 0
POL(new_compare7(x₁, x₂, x₃, x₄)) = 0
POL(new_compare8(x₁, x₂, x₃)) = 0
POL(new_compare9(x₁, x₂)) = 0
POL(new_merge(x₁, x₂, x₃)) = x₁
POL(new_merge0(x₁, x₂, x₃, x₄, x₅, x₆)) = 1 + x₃
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented: none

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge0(vz88, vz89, vz90, vz91, GT, ba) → new_merge(:(vz89, vz90), vz91, ba)
new_merge(:(vz780, vz781), :(vz7900, vz7901), bb) → new_merge0(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, bb), bb)

The TRS R consists of the following rules:

new_compare2(vz780, vz7900, bc) → error([])
new_compare(vz780, vz7900, app(ty_[], bd)) → new_compare3(vz780, vz7900, bd)
new_compare(vz780, vz7900, app(ty_Ratio, bc)) → new_compare2(vz780, vz7900, bc)
new_compare7(vz780, vz7900, bh, ca) → error([])
new_compare0(vz780, vz7900) → error([])
new_compare4(vz780, vz7900, be, bf, bg) → error([])
new_compare10(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Integer) → new_compare0(vz780, vz7900)
new_compare3(vz780, vz7900, bd) → error([])
new_compare(vz780, vz7900, ty_Float) → new_compare5(vz780, vz7900)
new_compare(vz780, vz7900, ty_Char) → new_compare13(vz780, vz7900)
new_compare13(Char(vz8100), Char(vz8000)) → new_primCmpNat0(vz8100, vz8000)
new_compare(vz780, vz7900, app(app(ty_Either, bh), ca)) → new_compare7(vz780, vz7900, bh, ca)
new_compare1(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Bool) → new_compare10(vz780, vz7900)
new_compare6(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_@0) → new_compare1(vz780, vz7900)
new_compare(vz780, vz7900, app(ty_Maybe, cb)) → new_compare8(vz780, vz7900, cb)
new_compare8(vz780, vz7900, cb) → error([])
new_compare5(vz780, vz7900) → error([])
new_primCmpNat0(Zero, Succ(vz80000)) → LT
new_compare12(vz780, vz7900) → error([])
new_compare(vz780, vz7900, ty_Double) → new_compare12(vz780, vz7900)
new_compare(vz780, vz7900, app(app(app(ty_@3, be), bf), bg)) → new_compare4(vz780, vz7900, be, bf, bg)
new_compare9(vz780, vz7900) → error([])
new_primCmpNat0(Succ(vz81000), Succ(vz80000)) → new_primCmpNat0(vz81000, vz80000)
new_compare(vz780, vz7900, app(app(ty_@2, cc), cd)) → new_compare11(vz780, vz7900, cc, cd)
new_compare11(vz780, vz7900, cc, cd) → error([])
new_primCmpNat0(Zero, Zero) → EQ
new_compare(vz780, vz7900, ty_Ordering) → new_compare6(vz780, vz7900)
new_compare(vz780, vz7900, ty_Int) → new_compare9(vz780, vz7900)
new_primCmpNat0(Succ(vz81000), Zero) → GT

The set Q consists of the following terms:

new_primCmpNat0(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare3(x0, x1, x2)
new_compare5(x0, x1)
new_compare1(x0, x1)
new_primCmpNat0(Zero, Zero)
new_compare(x0, x1, ty_Bool)
new_compare(x0, x1, ty_Float)
new_primCmpNat0(Succ(x0), Succ(x1))
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, ty_Ordering)
new_compare12(x0, x1)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare(x0, x1, app(ty_[], x2))
new_compare10(x0, x1)
new_compare(x0, x1, ty_@0)
new_compare2(x0, x1, x2)
new_compare4(x0, x1, x2, x3, x4)
new_compare0(x0, x1)
new_compare11(x0, x1, x2, x3)
new_compare(x0, x1, ty_Int)
new_compare(x0, x1, ty_Char)
new_compare9(x0, x1)
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare8(x0, x1, x2)
new_compare7(x0, x1, x2, x3)
new_compare(x0, x1, ty_Integer)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare13(Char(x0), Char(x1))
new_primCmpNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_merge(:(vz780, vz781), :(vz7900, vz7901), bb) → new_merge0(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, bb), bb)
The graph contains the following edges 2 > 1, 1 > 2, 1 > 3, 2 > 4, 3 >= 6
new_merge0(vz88, vz89, vz90, vz91, GT, ba) → new_merge(:(vz89, vz90), vz91, ba)
The graph contains the following edges 4 >= 2, 6 >= 3

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_merge_pairs(:(vz79110, :(vz791110, vz791111)), ba) → new_merge_pairs(vz791111, ba)

From the DPs we obtained the following set of size-change graphs:

new_merge_pairs(:(vz79110, :(vz791110, vz791111)), ba) → new_merge_pairs(vz791111, ba)
The graph contains the following edges 1 > 1, 2 >= 2

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz78, :(vz790, []), ba) → new_mergesort'(new_merge2(vz78, vz790, ba), [], ba)
new_mergesort'(vz78, :(vz790, :(vz7910, vz7911)), ba) → new_mergesort'(new_merge1(vz78, vz790, vz7910, ba), new_merge_pairs0(vz7911, ba), ba)

The TRS R consists of the following rules:

new_compare2(vz780, vz7900, bb) → error([])
new_compare(vz780, vz7900, app(ty_[], bc)) → new_compare3(vz780, vz7900, bc)
new_compare(vz780, vz7900, app(ty_Ratio, bb)) → new_compare2(vz780, vz7900, bb)
new_compare7(vz780, vz7900, bh, ca) → error([])
new_compare0(vz780, vz7900) → error([])
new_compare10(vz780, vz7900) → error([])
new_merge00(vz88, vz89, vz90, vz91, LT, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_compare3(vz780, vz7900, bc) → error([])
new_merge_pairs0(:(vz79110, :(vz791110, vz791111)), ba) → :(new_merge2(vz79110, vz791110, ba), new_merge_pairs0(vz791111, ba))
new_compare14(vz7900, vz79100, ty_Bool) → new_compare10(vz7900, vz79100)
new_merge1(vz78, [], :(vz79100, vz79101), ba) → new_merge2(vz78, :(vz79100, vz79101), ba)
new_compare(vz780, vz7900, ty_Char) → new_compare13(vz780, vz7900)
new_merge_pairs0(:(vz79110, []), ba) → :(vz79110, [])
new_compare(vz780, vz7900, app(app(ty_Either, bh), ca)) → new_compare7(vz780, vz7900, bh, ca)
new_merge1(vz78, :(vz7900, vz7901), :(vz79100, vz79101), ba) → new_merge2(vz78, new_merge00(vz79100, vz7900, vz7901, vz79101, new_compare14(vz7900, vz79100, ba), ba), ba)
new_compare(vz780, vz7900, app(ty_Maybe, cb)) → new_compare8(vz780, vz7900, cb)
new_compare14(vz7900, vz79100, ty_Ordering) → new_compare6(vz7900, vz79100)
new_merge00(vz88, vz89, vz90, vz91, GT, bg) → :(vz88, new_merge2(:(vz89, vz90), vz91, bg))
new_compare(vz780, vz7900, ty_Double) → new_compare12(vz780, vz7900)
new_compare(vz780, vz7900, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz780, vz7900, bd, be, bf)
new_compare9(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz7900, vz79100, bd, be, bf)
new_primCmpNat0(Succ(vz81000), Succ(vz80000)) → new_primCmpNat0(vz81000, vz80000)
new_compare11(vz780, vz7900, cc, cd) → error([])
new_compare(vz780, vz7900, ty_Ordering) → new_compare6(vz780, vz7900)
new_merge2([], :(vz7900, vz7901), ba) → :(vz7900, vz7901)
new_compare14(vz7900, vz79100, ty_Integer) → new_compare0(vz7900, vz79100)
new_merge_pairs0([], ba) → []
new_compare14(vz7900, vz79100, ty_Int) → new_compare9(vz7900, vz79100)
new_compare14(vz7900, vz79100, app(ty_Maybe, cb)) → new_compare8(vz7900, vz79100, cb)
new_compare4(vz780, vz7900, bd, be, bf) → error([])
new_compare(vz780, vz7900, ty_Integer) → new_compare0(vz780, vz7900)
new_merge1(vz78, vz790, [], ba) → new_merge2(vz78, vz790, ba)
new_merge2(:(vz780, vz781), :(vz7900, vz7901), ba) → new_merge00(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, ba), ba)
new_compare(vz780, vz7900, ty_Float) → new_compare5(vz780, vz7900)
new_compare14(vz7900, vz79100, ty_@0) → new_compare1(vz7900, vz79100)
new_compare14(vz7900, vz79100, ty_Float) → new_compare5(vz7900, vz79100)
new_compare13(Char(vz8100), Char(vz8000)) → new_primCmpNat0(vz8100, vz8000)
new_merge2(vz78, [], ba) → vz78
new_compare14(vz7900, vz79100, app(app(ty_Either, bh), ca)) → new_compare7(vz7900, vz79100, bh, ca)
new_compare1(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Double) → new_compare12(vz7900, vz79100)
new_compare(vz780, vz7900, ty_Bool) → new_compare10(vz780, vz7900)
new_compare(vz780, vz7900, ty_@0) → new_compare1(vz780, vz7900)
new_compare6(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(ty_@2, cc), cd)) → new_compare11(vz7900, vz79100, cc, cd)
new_compare8(vz780, vz7900, cb) → error([])
new_compare5(vz780, vz7900) → error([])
new_primCmpNat0(Zero, Succ(vz80000)) → LT
new_compare12(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Char) → new_compare13(vz7900, vz79100)
new_compare(vz780, vz7900, app(app(ty_@2, cc), cd)) → new_compare11(vz780, vz7900, cc, cd)
new_compare14(vz7900, vz79100, app(ty_Ratio, bb)) → new_compare2(vz7900, vz79100, bb)
new_merge00(vz88, vz89, vz90, vz91, EQ, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_primCmpNat0(Zero, Zero) → EQ
new_compare(vz780, vz7900, ty_Int) → new_compare9(vz780, vz7900)
new_primCmpNat0(Succ(vz81000), Zero) → GT
new_compare14(vz7900, vz79100, app(ty_[], bc)) → new_compare3(vz7900, vz79100, bc)

The set Q consists of the following terms:

new_primCmpNat0(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare5(x0, x1)
new_merge2(x0, [], x1)
new_compare1(x0, x1)
new_compare3(x0, x1, x2)
new_compare(x0, x1, ty_Float)
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Ordering)
new_compare12(x0, x1)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Integer)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare14(x0, x1, ty_Char)
new_compare11(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Int)
new_compare9(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare4(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1, x2)
new_compare7(x0, x1, x2, x3)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(x0, x1, x2)
new_compare(x0, x1, ty_Integer)
new_compare13(Char(x0), Char(x1))
new_compare14(x0, x1, ty_Int)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat0(Zero, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, ty_Bool)
new_primCmpNat0(Succ(x0), Succ(x1))
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge_pairs0(:(x0, []), x1)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, ty_@0)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_@0)
new_primCmpNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

new_mergesort'(vz78, :(vz790, :(vz7910, vz7911)), ba) → new_mergesort'(new_merge1(vz78, vz790, vz7910, ba), new_merge_pairs0(vz7911, ba), ba)

The TRS R consists of the following rules:

new_compare2(vz780, vz7900, bb) → error([])
new_compare(vz780, vz7900, app(ty_[], bc)) → new_compare3(vz780, vz7900, bc)
new_compare(vz780, vz7900, app(ty_Ratio, bb)) → new_compare2(vz780, vz7900, bb)
new_compare7(vz780, vz7900, bh, ca) → error([])
new_compare0(vz780, vz7900) → error([])
new_compare10(vz780, vz7900) → error([])
new_merge00(vz88, vz89, vz90, vz91, LT, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_compare3(vz780, vz7900, bc) → error([])
new_merge_pairs0(:(vz79110, :(vz791110, vz791111)), ba) → :(new_merge2(vz79110, vz791110, ba), new_merge_pairs0(vz791111, ba))
new_compare14(vz7900, vz79100, ty_Bool) → new_compare10(vz7900, vz79100)
new_merge1(vz78, [], :(vz79100, vz79101), ba) → new_merge2(vz78, :(vz79100, vz79101), ba)
new_compare(vz780, vz7900, ty_Char) → new_compare13(vz780, vz7900)
new_merge_pairs0(:(vz79110, []), ba) → :(vz79110, [])
new_compare(vz780, vz7900, app(app(ty_Either, bh), ca)) → new_compare7(vz780, vz7900, bh, ca)
new_merge1(vz78, :(vz7900, vz7901), :(vz79100, vz79101), ba) → new_merge2(vz78, new_merge00(vz79100, vz7900, vz7901, vz79101, new_compare14(vz7900, vz79100, ba), ba), ba)
new_compare(vz780, vz7900, app(ty_Maybe, cb)) → new_compare8(vz780, vz7900, cb)
new_compare14(vz7900, vz79100, ty_Ordering) → new_compare6(vz7900, vz79100)
new_merge00(vz88, vz89, vz90, vz91, GT, bg) → :(vz88, new_merge2(:(vz89, vz90), vz91, bg))
new_compare(vz780, vz7900, ty_Double) → new_compare12(vz780, vz7900)
new_compare(vz780, vz7900, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz780, vz7900, bd, be, bf)
new_compare9(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz7900, vz79100, bd, be, bf)
new_primCmpNat0(Succ(vz81000), Succ(vz80000)) → new_primCmpNat0(vz81000, vz80000)
new_compare11(vz780, vz7900, cc, cd) → error([])
new_compare(vz780, vz7900, ty_Ordering) → new_compare6(vz780, vz7900)
new_merge2([], :(vz7900, vz7901), ba) → :(vz7900, vz7901)
new_compare14(vz7900, vz79100, ty_Integer) → new_compare0(vz7900, vz79100)
new_merge_pairs0([], ba) → []
new_compare14(vz7900, vz79100, ty_Int) → new_compare9(vz7900, vz79100)
new_compare14(vz7900, vz79100, app(ty_Maybe, cb)) → new_compare8(vz7900, vz79100, cb)
new_compare4(vz780, vz7900, bd, be, bf) → error([])
new_compare(vz780, vz7900, ty_Integer) → new_compare0(vz780, vz7900)
new_merge1(vz78, vz790, [], ba) → new_merge2(vz78, vz790, ba)
new_merge2(:(vz780, vz781), :(vz7900, vz7901), ba) → new_merge00(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, ba), ba)
new_compare(vz780, vz7900, ty_Float) → new_compare5(vz780, vz7900)
new_compare14(vz7900, vz79100, ty_@0) → new_compare1(vz7900, vz79100)
new_compare14(vz7900, vz79100, ty_Float) → new_compare5(vz7900, vz79100)
new_compare13(Char(vz8100), Char(vz8000)) → new_primCmpNat0(vz8100, vz8000)
new_merge2(vz78, [], ba) → vz78
new_compare14(vz7900, vz79100, app(app(ty_Either, bh), ca)) → new_compare7(vz7900, vz79100, bh, ca)
new_compare1(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Double) → new_compare12(vz7900, vz79100)
new_compare(vz780, vz7900, ty_Bool) → new_compare10(vz780, vz7900)
new_compare(vz780, vz7900, ty_@0) → new_compare1(vz780, vz7900)
new_compare6(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(ty_@2, cc), cd)) → new_compare11(vz7900, vz79100, cc, cd)
new_compare8(vz780, vz7900, cb) → error([])
new_compare5(vz780, vz7900) → error([])
new_primCmpNat0(Zero, Succ(vz80000)) → LT
new_compare12(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Char) → new_compare13(vz7900, vz79100)
new_compare(vz780, vz7900, app(app(ty_@2, cc), cd)) → new_compare11(vz780, vz7900, cc, cd)
new_compare14(vz7900, vz79100, app(ty_Ratio, bb)) → new_compare2(vz7900, vz79100, bb)
new_merge00(vz88, vz89, vz90, vz91, EQ, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_primCmpNat0(Zero, Zero) → EQ
new_compare(vz780, vz7900, ty_Int) → new_compare9(vz780, vz7900)
new_primCmpNat0(Succ(vz81000), Zero) → GT
new_compare14(vz7900, vz79100, app(ty_[], bc)) → new_compare3(vz7900, vz79100, bc)

The set Q consists of the following terms:

new_primCmpNat0(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare5(x0, x1)
new_merge2(x0, [], x1)
new_compare1(x0, x1)
new_compare3(x0, x1, x2)
new_compare(x0, x1, ty_Float)
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Ordering)
new_compare12(x0, x1)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Integer)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare14(x0, x1, ty_Char)
new_compare11(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Int)
new_compare9(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare4(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1, x2)
new_compare7(x0, x1, x2, x3)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(x0, x1, x2)
new_compare(x0, x1, ty_Integer)
new_compare13(Char(x0), Char(x1))
new_compare14(x0, x1, ty_Int)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat0(Zero, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, ty_Bool)
new_primCmpNat0(Succ(x0), Succ(x1))
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge_pairs0(:(x0, []), x1)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, ty_@0)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_@0)
new_primCmpNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

new_mergesort'(vz78, :(vz790, :(vz7910, vz7911)), ba) → new_mergesort'(new_merge1(vz78, vz790, vz7910, ba), new_merge_pairs0(vz7911, ba), ba)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:

POL(:(x₁, x₂)) = 1 + x₂
POL(Char(x₁)) = 0
POL(EQ) = 0
POL(GT) = 0
POL(LT) = 0
POL(Succ(x₁)) = 0
POL(Zero) = 0
POL([]) = 1
POL(app(x₁, x₂)) = 1 + x₁ + x₂
POL(error(x₁)) = 0
POL(new_compare(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(new_compare0(x₁, x₂)) = 1
POL(new_compare1(x₁, x₂)) = 1
POL(new_compare10(x₁, x₂)) = 1
POL(new_compare11(x₁, x₂, x₃, x₄)) = 1
POL(new_compare12(x₁, x₂)) = 1
POL(new_compare13(x₁, x₂)) = 1
POL(new_compare14(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(new_compare2(x₁, x₂, x₃)) = 1
POL(new_compare3(x₁, x₂, x₃)) = 1
POL(new_compare4(x₁, x₂, x₃, x₄, x₅)) = 1
POL(new_compare5(x₁, x₂)) = 1
POL(new_compare6(x₁, x₂)) = 1
POL(new_compare7(x₁, x₂, x₃, x₄)) = 1
POL(new_compare8(x₁, x₂, x₃)) = 1
POL(new_compare9(x₁, x₂)) = 1 + x₁
POL(new_merge00(x₁, x₂, x₃, x₄, x₅, x₆)) = 0
POL(new_merge1(x₁, x₂, x₃, x₄)) = 0
POL(new_merge2(x₁, x₂, x₃)) = 0
POL(new_merge_pairs0(x₁, x₂)) = 1 + x₁
POL(new_mergesort'(x₁, x₂, x₃)) = x₂
POL(new_primCmpNat0(x₁, x₂)) = 0
POL(ty_@0) = 1
POL(ty_@2) = 1
POL(ty_@3) = 0
POL(ty_Bool) = 1
POL(ty_Char) = 1
POL(ty_Double) = 1
POL(ty_Either) = 1
POL(ty_Float) = 1
POL(ty_Int) = 1
POL(ty_Integer) = 1
POL(ty_Maybe) = 0
POL(ty_Ordering) = 1
POL(ty_Ratio) = 0
POL(ty_[]) = 0

The following usable rules [17] were oriented:

new_merge_pairs0(:(vz79110, :(vz791110, vz791111)), ba) → :(new_merge2(vz79110, vz791110, ba), new_merge_pairs0(vz791111, ba))
new_merge_pairs0(:(vz79110, []), ba) → :(vz79110, [])
new_merge_pairs0([], ba) → []

↳ HASKELL

  ↳ CR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

new_compare2(vz780, vz7900, bb) → error([])
new_compare(vz780, vz7900, app(ty_[], bc)) → new_compare3(vz780, vz7900, bc)
new_compare(vz780, vz7900, app(ty_Ratio, bb)) → new_compare2(vz780, vz7900, bb)
new_compare7(vz780, vz7900, bh, ca) → error([])
new_compare0(vz780, vz7900) → error([])
new_compare10(vz780, vz7900) → error([])
new_merge00(vz88, vz89, vz90, vz91, LT, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_compare3(vz780, vz7900, bc) → error([])
new_merge_pairs0(:(vz79110, :(vz791110, vz791111)), ba) → :(new_merge2(vz79110, vz791110, ba), new_merge_pairs0(vz791111, ba))
new_compare14(vz7900, vz79100, ty_Bool) → new_compare10(vz7900, vz79100)
new_merge1(vz78, [], :(vz79100, vz79101), ba) → new_merge2(vz78, :(vz79100, vz79101), ba)
new_compare(vz780, vz7900, ty_Char) → new_compare13(vz780, vz7900)
new_merge_pairs0(:(vz79110, []), ba) → :(vz79110, [])
new_compare(vz780, vz7900, app(app(ty_Either, bh), ca)) → new_compare7(vz780, vz7900, bh, ca)
new_merge1(vz78, :(vz7900, vz7901), :(vz79100, vz79101), ba) → new_merge2(vz78, new_merge00(vz79100, vz7900, vz7901, vz79101, new_compare14(vz7900, vz79100, ba), ba), ba)
new_compare(vz780, vz7900, app(ty_Maybe, cb)) → new_compare8(vz780, vz7900, cb)
new_compare14(vz7900, vz79100, ty_Ordering) → new_compare6(vz7900, vz79100)
new_merge00(vz88, vz89, vz90, vz91, GT, bg) → :(vz88, new_merge2(:(vz89, vz90), vz91, bg))
new_compare(vz780, vz7900, ty_Double) → new_compare12(vz780, vz7900)
new_compare(vz780, vz7900, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz780, vz7900, bd, be, bf)
new_compare9(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(app(ty_@3, bd), be), bf)) → new_compare4(vz7900, vz79100, bd, be, bf)
new_primCmpNat0(Succ(vz81000), Succ(vz80000)) → new_primCmpNat0(vz81000, vz80000)
new_compare11(vz780, vz7900, cc, cd) → error([])
new_compare(vz780, vz7900, ty_Ordering) → new_compare6(vz780, vz7900)
new_merge2([], :(vz7900, vz7901), ba) → :(vz7900, vz7901)
new_compare14(vz7900, vz79100, ty_Integer) → new_compare0(vz7900, vz79100)
new_merge_pairs0([], ba) → []
new_compare14(vz7900, vz79100, ty_Int) → new_compare9(vz7900, vz79100)
new_compare14(vz7900, vz79100, app(ty_Maybe, cb)) → new_compare8(vz7900, vz79100, cb)
new_compare4(vz780, vz7900, bd, be, bf) → error([])
new_compare(vz780, vz7900, ty_Integer) → new_compare0(vz780, vz7900)
new_merge1(vz78, vz790, [], ba) → new_merge2(vz78, vz790, ba)
new_merge2(:(vz780, vz781), :(vz7900, vz7901), ba) → new_merge00(vz7900, vz780, vz781, vz7901, new_compare(vz780, vz7900, ba), ba)
new_compare(vz780, vz7900, ty_Float) → new_compare5(vz780, vz7900)
new_compare14(vz7900, vz79100, ty_@0) → new_compare1(vz7900, vz79100)
new_compare14(vz7900, vz79100, ty_Float) → new_compare5(vz7900, vz79100)
new_compare13(Char(vz8100), Char(vz8000)) → new_primCmpNat0(vz8100, vz8000)
new_merge2(vz78, [], ba) → vz78
new_compare14(vz7900, vz79100, app(app(ty_Either, bh), ca)) → new_compare7(vz7900, vz79100, bh, ca)
new_compare1(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Double) → new_compare12(vz7900, vz79100)
new_compare(vz780, vz7900, ty_Bool) → new_compare10(vz780, vz7900)
new_compare(vz780, vz7900, ty_@0) → new_compare1(vz780, vz7900)
new_compare6(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, app(app(ty_@2, cc), cd)) → new_compare11(vz7900, vz79100, cc, cd)
new_compare8(vz780, vz7900, cb) → error([])
new_compare5(vz780, vz7900) → error([])
new_primCmpNat0(Zero, Succ(vz80000)) → LT
new_compare12(vz780, vz7900) → error([])
new_compare14(vz7900, vz79100, ty_Char) → new_compare13(vz7900, vz79100)
new_compare(vz780, vz7900, app(app(ty_@2, cc), cd)) → new_compare11(vz780, vz7900, cc, cd)
new_compare14(vz7900, vz79100, app(ty_Ratio, bb)) → new_compare2(vz7900, vz79100, bb)
new_merge00(vz88, vz89, vz90, vz91, EQ, bg) → :(vz89, new_merge2(vz90, :(vz88, vz91), bg))
new_primCmpNat0(Zero, Zero) → EQ
new_compare(vz780, vz7900, ty_Int) → new_compare9(vz780, vz7900)
new_primCmpNat0(Succ(vz81000), Zero) → GT
new_compare14(vz7900, vz79100, app(ty_[], bc)) → new_compare3(vz7900, vz79100, bc)

The set Q consists of the following terms:

new_primCmpNat0(Succ(x0), Zero)
new_compare6(x0, x1)
new_compare14(x0, x1, ty_Ordering)
new_compare5(x0, x1)
new_merge2(x0, [], x1)
new_compare1(x0, x1)
new_compare3(x0, x1, x2)
new_compare(x0, x1, ty_Float)
new_merge2([], :(x0, x1), x2)
new_compare(x0, x1, app(app(ty_Either, x2), x3))
new_compare14(x0, x1, ty_Double)
new_compare(x0, x1, ty_Ordering)
new_compare12(x0, x1)
new_compare(x0, x1, app(app(ty_@2, x2), x3))
new_compare10(x0, x1)
new_compare(x0, x1, app(ty_[], x2))
new_compare14(x0, x1, ty_Integer)
new_merge2(:(x0, x1), :(x2, x3), x4)
new_compare14(x0, x1, ty_Char)
new_compare11(x0, x1, x2, x3)
new_merge00(x0, x1, x2, x3, EQ, x4)
new_compare(x0, x1, ty_Int)
new_compare9(x0, x1)
new_compare(x0, x1, ty_Char)
new_compare4(x0, x1, x2, x3, x4)
new_compare(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare8(x0, x1, x2)
new_compare7(x0, x1, x2, x3)
new_compare14(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_compare2(x0, x1, x2)
new_compare(x0, x1, ty_Integer)
new_compare13(Char(x0), Char(x1))
new_compare14(x0, x1, ty_Int)
new_merge_pairs0(:(x0, :(x1, x2)), x3)
new_merge00(x0, x1, x2, x3, LT, x4)
new_merge_pairs0([], x0)
new_compare14(x0, x1, app(ty_Maybe, x2))
new_primCmpNat0(Zero, Zero)
new_merge00(x0, x1, x2, x3, GT, x4)
new_compare(x0, x1, ty_Bool)
new_primCmpNat0(Succ(x0), Succ(x1))
new_compare(x0, x1, ty_Double)
new_compare(x0, x1, app(ty_Ratio, x2))
new_compare14(x0, x1, app(app(ty_Either, x2), x3))
new_merge1(x0, [], :(x1, x2), x3)
new_compare14(x0, x1, ty_Bool)
new_compare14(x0, x1, app(ty_Ratio, x2))
new_merge_pairs0(:(x0, []), x1)
new_compare14(x0, x1, ty_Float)
new_compare(x0, x1, ty_@0)
new_merge1(x0, x1, [], x2)
new_compare14(x0, x1, app(app(ty_@2, x2), x3))
new_merge1(x0, :(x1, x2), :(x3, x4), x5)
new_compare0(x0, x1)
new_compare14(x0, x1, app(ty_[], x2))
new_compare(x0, x1, app(ty_Maybe, x2))
new_compare14(x0, x1, ty_@0)
new_primCmpNat0(Zero, Succ(x0))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

case	cmp x y of
	GT	→ y : merge cmp (x : xs) ys
	_	→ x : merge cmp xs (y : ys)

merge0	y cmp x xs ys GT	= y : merge cmp (x : xs) ys
merge0	y cmp x xs ys _	= x : merge cmp xs (y : ys)